\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$, $B$, $C$:Type, ${\it Ia}$:AbsInterface($A$), ${\it Ib}$:AbsInterface($B$), ${\it Ic}$:AbsInterface($C$),\+
\\[0ex]$f_{1}$:(E(${\it Ia}$)$\rightarrow$$B$), $f_{2}$:($B$$\rightarrow$$C$).
\-\\[0ex](glued(${\it es}$; $B$; $f_{1}$; ${\it Ia}$; ${\it Ib}$) \& glued(${\it es}$; $C$; ($\lambda$$e$.$f_{2}$(${\it Ib}$($e$))); ${\it Ib}$; ${\it Ic}$))
\\[0ex]$\Rightarrow$ glued(${\it es}$; $C$; ($f_{2}$ o $f_{1}$); ${\it Ia}$; ${\it Ic}$)
\end{tabbing}